$\vdash$  $\forall$$T$:Type, $l_{1}$, $l_{2}$:($T$ List). fseg($T$;$l_{1}$;$l_{2}$) $\Rightarrow$ ($\parallel$$l_{1}$$\parallel$ $\leq$ $\parallel$$l_{2}$$\parallel$)